Nuprl Lemma : l_before_member2 11,40

T:Type, L:(T List), a,b:T. l_before(abLT (a  L
latex


Definitionst  T, l_before(xylT), P  Q, x:AB(x), P  Q, P  Q, P  Q, True, P  Q, prop{i:l}
Lemmassublist wf, member iff sublist, sublist transitivity, cons sublist cons, nil sublist, and functionality wrt iff, or functionality wrt iff, true wf

origin